In a multiprocessing computing environment, more than one process may actively use the resources available in the computing environment. To avoid corruption of a resource due to the concurrent use or modification by multiple processes, a process may lock a resource and release the lock after the process has finished using the process.
In some situations, a deadlock occurs when two processes or two elements (e.g., threads) in a process are each waiting for the other to release a lock, before one can continue. Occurrence of a deadlock is disruptive. Thus, software applications and multiprocessing environments in which the applications operate are typically tested to determine and prevent deadlocks.
A methodology called a lock discipline may be used to avoid deadlock. A lock discipline defines the order in which a plurality of processes or threads may lock a plurality of resources in a concurrent/parallel processing environment. According to the lock discipline, when several locks need to be taken together, each lock is taken in a predefined order, so that all active processes or threads may share resources without creating a deadlock situation.
A directed graph, having multiple nodes and edges that connect the nodes, can be implemented to graphically represent a lock discipline. Nodes in the graph represent the locks, and an edge connecting, for example, a first node A to a second node B represents the possibility of taking consecutive locks A and B (i.e., B nested within A). Once a lock discipline is defined for a given system, it is desirable to have a tool that will indicate whether the system indeed adheres to the lock discipline.
NASA's Java PathFinder (JPF)™ is one such tool that uses dynamic analysis to monitor locks taken by a plurality of threads at runtime. JPF uses a special Java Virtual Machine (JVM)™ to determine the threads and the order in which the locks are taken, so that violations of lock discipline can be revealed. JPF is especially suited for analyzing multi-threaded Java applications, where normal testing usually falls short. JPF can find deadlocks and violations of Boolean assertions stated by the programmer in a special assertion language. (See Visser, Havelund, Brat, Park and Lerda: “Model Checking Programs,” Journal of Automated Software Engineering, 10(2): 203-232, April 2003.)
Microsoft's Driver Verifier™ is another tool that can monitor kernel-mode drivers and graphics drivers to verify that they are not making illegal function calls or causing system corruption. This tool can perform a large number of checks on the mentioned drivers, as well as subject them to a variety of stresses and test to flush out improper behavior. (See http://msdn.microsoft.com/library/)
A test suite for determining violation of lock discipline is typically composed of many small tests. Each test is run by a distinct process that activates selected short test paths. The above tools identify violations of lock discipline during test runtime, but only look within the scope of one process during each test run. As such, if a cycle in the directed graph is caused by lock sequences from two different test runs, the above tools cannot reveal it.
Furthermore, these tools are applicable only to inter-thread locks within one process (i.e., mutexes) and therefore cannot be easily utilized in other environments. For example, the above tools cannot be successfully applied to determine deadlock for locks used to synchronize processes, such as file locks.
Thus, deadlock analysis and prevention methods and systems are needed that can overcome the aforementioned shortcomings by revealing deadlocks across different test runs.